gov.nasa.jpf.rtsj.test
Class TestClient

java.lang.Object
  gov.nasa.jpf.rtsj.test.TestClient

All Implemented Interfaces:

gov.nasa.jpf.JPFListener, gov.nasa.jpf.SearchListener, gov.nasa.jpf.VMListener

public class TestClient

extends java.lang.Object

implements gov.nasa.jpf.VMListener, gov.nasa.jpf.SearchListener

A test harness (main program) for running a RTSJ program under JPF.

Author:

gary

Nested Class Summary

(package private) class

TestClient.StackFrame An internal class for frames on the backtracking stack maintained by this class for backtracking quantitative observations when the JPF JVM backtracks

Field Summary

(package private) int	backTracks Backtracks (not backtracked)
static AbsoluteTime[]	byteCodeCosts Code per byte code as AbsoluteTime
(package private) int[]	byteCodeCounts Running count of executions per byte code (backtracked)
static java.lang.String[]	byteCodeMnemonics
(package private) int	classesLoaded Classes loaded on this path (backtracked)
(package private) int	gcsBegun Garbage collections begun (not backtracked)
(package private) int	gcsEnded Garbage collections ended (not backtracked)
(package private) int	instructionCount Instructions executed on this path (backtracked)
static int	invokeLevel Counts invoke level (number of invoke byte codes minus number of return byte codes.
static boolean	invokeTracing Is invoke tracing currently on?
(package private) static int	lastThreadIndex
(package private) int	objectsCreated Objects created on this path (backtracked)
(package private) int	objectsReleased Objects released on this path (backtracked)
static java.util.Random	random An instance of java.util.Random usable throughout the JPF run
(package private) java.util.Stack	stack The local backtracking stack, for maintaining path statistics
(package private) boolean	stackGrowing true indicates last stateAdvanced or stateBacktracked was stateAdvanced false indicates last stateAdvanced or stateBacktracked was stateBacktracked
(package private) int	stateDepth Current state depth (incremented on state advance, and backtracked on state backtracked)
(package private) int	statesProcessed States processed (not backtracked)
static TestClient	theTestClient Dynamic instance of TestClient accessed via MJI
(package private) int	threadsStarted Threads started on this path (backtracked)
(package private) int	threadsTerminated Threads terminated on this path (backtracked)
static AbsoluteTime	totalCost Total cost of this path (backtracked)

Constructor Summary

TestClient()
Constructor.

Method Summary

void	classLoaded(gov.nasa.jpf.VM vm) new class was loaded
static void	clearActivePhaseCost() Clear the active phase cost accumulator
void	exceptionThrown(gov.nasa.jpf.VM vm) exception was thrown
void	gcBegin(gov.nasa.jpf.VM vm) a garbage collection was begun.
void	gcEnd(gov.nasa.jpf.VM vm) a garbage collection ended
static long	getActivePhaseCostMillis()
static long	getActivePhaseCostNanos()
static int	getInstructionCount()
static long	getThreadRunCostMillis()
static long	getThreadRunCostNanos()
void	instructionExecuted(gov.nasa.jpf.VM vm) The listener invoked by the JPF JVM for each byte code executed.
static void	main(java.lang.String[] args) Main method.
static long	millisSinceEpoch()
static double	nextDouble()
static int	nextInt(int limit) Return an integer derived from the next pseudo random number draw.
void	objectCreated(gov.nasa.jpf.VM vm) new object was created
void	objectReleased(gov.nasa.jpf.VM vm) object was garbage collected (after potential finalization)
int	objectsInExistence() Count the number of objects in existence in the JPF model
static void	printExecutionStatistics() Print statistics of this run (path, if executing under JPF).
void	propertyViolated(gov.nasa.jpf.Search search) JPF encountered a property violation
void	reportByteCodeCounts() Print counts of each byte code executed by the JPF JVM
void	searchConstraintHit(gov.nasa.jpf.Search search) there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application
void	searchFinished(gov.nasa.jpf.Search search) we're done, either with or without a preceeding error
void	searchStarted(gov.nasa.jpf.Search search) we get this after we enter the search loop, but BEFORE the first forward
void	stateAdvanced(gov.nasa.jpf.Search search) the JPF state is advanced
void	stateBacktracked(gov.nasa.jpf.Search search) state was backtracked one step
void	stateProcessed(gov.nasa.jpf.Search search) state is fully explored
void	stateRestored(gov.nasa.jpf.Search search) a previously generated state was restored (can be on a completely different path)
void	threadStarted(gov.nasa.jpf.VM vm) new Thread entered run() method
void	threadTerminated(gov.nasa.jpf.VM vm) Thread exited run() method
static void	turnOffInvokeTracing() Turn off tracing of invoke byte codes (if running under JPF).
static void	turnOnInvokeTracing() Turn on tracing of invoke byte codes (if running under JPF).

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

instructionCount

int instructionCount

Instructions executed on this path (backtracked)

classesLoaded

int classesLoaded

Classes loaded on this path (backtracked)

objectsCreated

int objectsCreated

Objects created on this path (backtracked)

objectsReleased

int objectsReleased

Objects released on this path (backtracked)

threadsStarted

int threadsStarted

Threads started on this path (backtracked)

threadsTerminated

int threadsTerminated

Threads terminated on this path (backtracked)

gcsBegun

int gcsBegun

Garbage collections begun (not backtracked)

gcsEnded

int gcsEnded

Garbage collections ended (not backtracked)

stateDepth

int stateDepth

Current state depth (incremented on state advance, and backtracked on state backtracked)

statesProcessed

int statesProcessed

States processed (not backtracked)

backTracks

int backTracks

Backtracks (not backtracked)

byteCodeCounts

int[] byteCodeCounts

Running count of executions per byte code (backtracked)

stackGrowing

boolean stackGrowing

true indicates last stateAdvanced or stateBacktracked was stateAdvanced false indicates last stateAdvanced or stateBacktracked was stateBacktracked

lastThreadIndex

static int lastThreadIndex

stack

java.util.Stack stack

The local backtracking stack, for maintaining path statistics

random

public static final java.util.Random random

An instance of java.util.Random usable throughout the JPF run

theTestClient

public static TestClient theTestClient

Dynamic instance of TestClient accessed via MJI

byteCodeMnemonics

public static java.lang.String[] byteCodeMnemonics

byteCodeCosts

public static AbsoluteTime[] byteCodeCosts

Code per byte code as AbsoluteTime

totalCost

public static AbsoluteTime totalCost

Total cost of this path (backtracked)

invokeTracing

public static boolean invokeTracing

Is invoke tracing currently on?

invokeLevel

public static int invokeLevel

Counts invoke level (number of invoke byte codes minus number of return byte codes. Note this accounting is imprecise due to native methods, which have invoke byte codes but not return byte codes.

Constructor Detail

TestClient

public TestClient()

Constructor. An instance is constructed to hold observed byte counts.

Method Detail

main

public static void main(java.lang.String[] args)

Main method.

Parameters:

args - Takes two command line arguments:

• the name of the class whose static void main( String[] ) method should be invoked by JPF
• a boolean literal, where true indicates all orderings of events scheduled at the same time should be tried non-deterministically; otherwise, pick equal time events in FIFO order.

printExecutionStatistics

public static void printExecutionStatistics()

Print statistics of this run (path, if executing under JPF).

instructionExecuted

public void instructionExecuted(gov.nasa.jpf.VM vm)

The listener invoked by the JPF JVM for each byte code executed.

Specified by:

instructionExecuted in interface gov.nasa.jpf.VMListener

threadStarted

public void threadStarted(gov.nasa.jpf.VM vm)

new Thread entered run() method

Specified by:

threadStarted in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

threadTerminated

public void threadTerminated(gov.nasa.jpf.VM vm)

Thread exited run() method

Specified by:

threadTerminated in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

classLoaded

public void classLoaded(gov.nasa.jpf.VM vm)

new class was loaded

Specified by:

classLoaded in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

objectCreated

public void objectCreated(gov.nasa.jpf.VM vm)

new object was created

Specified by:

objectCreated in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

objectReleased

public void objectReleased(gov.nasa.jpf.VM vm)

object was garbage collected (after potential finalization)

Specified by:

objectReleased in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

gcBegin

public void gcBegin(gov.nasa.jpf.VM vm)

a garbage collection was begun.

Specified by:

gcBegin in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

gcEnd

public void gcEnd(gov.nasa.jpf.VM vm)

a garbage collection ended

Specified by:

gcEnd in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

exceptionThrown

public void exceptionThrown(gov.nasa.jpf.VM vm)

exception was thrown

Specified by:

exceptionThrown in interface gov.nasa.jpf.VMListener

Parameters:

vm - the JPF virtual machine object

stateAdvanced

public void stateAdvanced(gov.nasa.jpf.Search search)

the JPF state is advanced

Specified by:

stateAdvanced in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

stateProcessed

public void stateProcessed(gov.nasa.jpf.Search search)

state is fully explored

Specified by:

stateProcessed in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

stateBacktracked

public void stateBacktracked(gov.nasa.jpf.Search search)

state was backtracked one step

Specified by:

stateBacktracked in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

stateRestored

public void stateRestored(gov.nasa.jpf.Search search)

a previously generated state was restored (can be on a completely different path)

Specified by:

stateRestored in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

propertyViolated

public void propertyViolated(gov.nasa.jpf.Search search)

JPF encountered a property violation

Specified by:

propertyViolated in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

searchStarted

public void searchStarted(gov.nasa.jpf.Search search)

we get this after we enter the search loop, but BEFORE the first forward

Specified by:

searchStarted in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

searchConstraintHit

public void searchConstraintHit(gov.nasa.jpf.Search search)

there was some contraint hit in the search, we back out could have been turned into a property, but usually is an attribute of the search, not the application

Specified by:

searchConstraintHit in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

searchFinished

public void searchFinished(gov.nasa.jpf.Search search)

we're done, either with or without a preceeding error

Specified by:

searchFinished in interface gov.nasa.jpf.SearchListener

Parameters:

search - the JPF Search object

objectsInExistence

public int objectsInExistence()

Count the number of objects in existence in the JPF model

Returns:

the number of objects in existence

reportByteCodeCounts

public void reportByteCodeCounts()

Print counts of each byte code executed by the JPF JVM

turnOnInvokeTracing

public static void turnOnInvokeTracing()

Turn on tracing of invoke byte codes (if running under JPF).

turnOffInvokeTracing

public static void turnOffInvokeTracing()

Turn off tracing of invoke byte codes (if running under JPF).

getInstructionCount

public static int getInstructionCount()

Returns:

the test client's instruction count

getActivePhaseCostMillis

public static long getActivePhaseCostMillis()

Returns:

the test client's active phase cost millis

getActivePhaseCostNanos

public static long getActivePhaseCostNanos()

Returns:

the test client's active phase cost nanos

getThreadRunCostMillis

public static long getThreadRunCostMillis()

Returns:

the test client's thread run cost millis

getThreadRunCostNanos

public static long getThreadRunCostNanos()

Returns:

the test client's thread run cost nanos

clearActivePhaseCost

public static void clearActivePhaseCost()

Clear the active phase cost accumulator

millisSinceEpoch

public static long millisSinceEpoch()

Returns:

millis since epoch start (Jan. 1, 1970?).

nextInt

public static int nextInt(int limit)

Return an integer derived from the next pseudo random number draw.

Parameters:

limit - the upper limit (non-inclusive) of the range

Returns:

a random int in [0, limit)

nextDouble

public static double nextDouble()